|
The simply typed lambda calculus (), a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor: that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical uses of the untyped lambda calculus, and it exhibits many desirable and interesting properties. The term ''simple type'' is also used to refer to extensions of the simply typed lambda calculus such as products, coproducts or natural numbers (System T) or even full recursion (like PCF). In contrast, systems which introduce polymorphic types (like System F) or dependent types (like the Logical Framework) are not considered ''simply typed''. The former are still considered ''simple'' because the Church encodings of such structures can be done using only and suitable type variables, while polymorphism and dependency cannot. == Syntax == In this article, we use and to range over types. Informally, the ''function type'' refers to the type of functions that, given an input of type , produce an output of type . By convention, associates to the right: we read as . To define the types, we begin by fixing a set of ''base types'', . These are sometimes called ''atomic types'' or ''type constants''. With this fixed, the syntax of types is: :. For example, if , then , , , , and are all valid types (among others). We also fix a set of ''term constants'' for the base types. For example, we might assume a base type nat, and the term constants could be the natural numbers. In the original presentation, Church used only two base types: for "the type of propositions" and for "the type of individuals". The type has no term constants, whereas has one term constant. Frequently the calculus with only one base type, usually , is considered. The syntax of the simply typed lambda calculus is essentially that of the lambda calculus itself. We write to denote that the variable is of type . The term syntax is then: : where is a term constant. That is, ''variable reference'', ''abstractions'', ''application'', and ''constant''. A variable reference is ''bound'' if it is inside of an abstraction binding . A term is ''closed'' if there are no unbound variables. Compare this to the syntax of untyped lambda calculus: : We see that in typed lambda calculus every function (''abstraction'') must specify the type of its argument. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「simply typed lambda calculus」の詳細全文を読む スポンサード リンク
|